Skip to content

[Merged by Bors] - feat(Projectivization/Independence): add lemma about independence#39778

Closed
Whysoserioushah wants to merge 3 commits into
leanprover-community:masterfrom
Whysoserioushah:edison/projgeo3
Closed

[Merged by Bors] - feat(Projectivization/Independence): add lemma about independence#39778
Whysoserioushah wants to merge 3 commits into
leanprover-community:masterfrom
Whysoserioushah:edison/projgeo3

Conversation

@Whysoserioushah

@Whysoserioushah Whysoserioushah commented May 24, 2026

Copy link
Copy Markdown
Collaborator

Open in Gitpod

@github-actions github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label May 24, 2026
@github-actions

github-actions Bot commented May 24, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 2fe22bb546

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ independent_mk_iff_LinearIndependent

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@Whysoserioushah Whysoserioushah added the easy < 20s of review time. See the lifecycle page for guidelines. label May 24, 2026
@Whysoserioushah Whysoserioushah mentioned this pull request May 24, 2026
Closed
1 task
riccardobrasca
riccardobrasca reviewed May 25, 2026
View reviewed changes

@riccardobrasca riccardobrasca left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors d+

Comment thread Mathlib/LinearAlgebra/Projectivization/Independence.lean Outdated
Comment thread Mathlib/LinearAlgebra/Projectivization/Independence.lean Outdated
@mathlib-bors

mathlib-bors Bot commented May 25, 2026

Copy link
Copy Markdown
Contributor

✌️ Whysoserioushah can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 25, 2026
Whysoserioushah and others added 2 commits May 25, 2026 15:20
@Whysoserioushah @riccardobrasca
Update Mathlib/LinearAlgebra/Projectivization/Independence.lean
04a4773 
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@Whysoserioushah
change name
2fe22bb
@Whysoserioushah

Whysoserioushah commented May 25, 2026

Copy link
Copy Markdown
Collaborator Author

bors r+

mathlib-bors Bot pushed a commit that referenced this pull request May 25, 2026
@Whysoserioushah
feat(Projectivization/Independence): add lemma about independence (#3…
8bfad47 
…9778)
@ocfnash

ocfnash commented May 25, 2026

Copy link
Copy Markdown
Contributor

Could this lemma be simp?

No need to stop bors but would be nice to add this in a follow-up PR if the simpNF linter allows it.

@mathlib-bors

mathlib-bors Bot commented May 25, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(Projectivization/Independence): add lemma about independence [Merged by Bors] - feat(Projectivization/Independence): add lemma about independence May 25, 2026
@mathlib-bors mathlib-bors Bot closed this May 25, 2026
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@Whysoserioushah @b-mehta
feat(Projectivization/Independence): add lemma about independence (le…
0c84444 
…anprover-community#39778)
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@Whysoserioushah @Bergschaf
feat(Projectivization/Independence): add lemma about independence (le…
ecbb77c 
…anprover-community#39778)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@riccardobrasca riccardobrasca riccardobrasca left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Whysoserioushah @ocfnash @riccardobrasca